not(true) → false
not(false) → true
evenodd(x, 0) → not(evenodd(x, s(0)))
evenodd(0, s(0)) → false
evenodd(s(x), s(0)) → evenodd(x, 0)
↳ QTRS
↳ DependencyPairsProof
not(true) → false
not(false) → true
evenodd(x, 0) → not(evenodd(x, s(0)))
evenodd(0, s(0)) → false
evenodd(s(x), s(0)) → evenodd(x, 0)
EVENODD(x, 0) → NOT(evenodd(x, s(0)))
EVENODD(x, 0) → EVENODD(x, s(0))
EVENODD(s(x), s(0)) → EVENODD(x, 0)
not(true) → false
not(false) → true
evenodd(x, 0) → not(evenodd(x, s(0)))
evenodd(0, s(0)) → false
evenodd(s(x), s(0)) → evenodd(x, 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
EVENODD(x, 0) → NOT(evenodd(x, s(0)))
EVENODD(x, 0) → EVENODD(x, s(0))
EVENODD(s(x), s(0)) → EVENODD(x, 0)
not(true) → false
not(false) → true
evenodd(x, 0) → not(evenodd(x, s(0)))
evenodd(0, s(0)) → false
evenodd(s(x), s(0)) → evenodd(x, 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
EVENODD(x, 0) → EVENODD(x, s(0))
EVENODD(s(x), s(0)) → EVENODD(x, 0)
not(true) → false
not(false) → true
evenodd(x, 0) → not(evenodd(x, s(0)))
evenodd(0, s(0)) → false
evenodd(s(x), s(0)) → evenodd(x, 0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EVENODD(s(x), s(0)) → EVENODD(x, 0)
Used ordering: Polynomial interpretation [25,35]:
EVENODD(x, 0) → EVENODD(x, s(0))
The value of delta used in the strict ordering is 8.
POL(EVENODD(x1, x2)) = (4)x_1
POL(s(x1)) = 2 + (2)x_1
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
EVENODD(x, 0) → EVENODD(x, s(0))
not(true) → false
not(false) → true
evenodd(x, 0) → not(evenodd(x, s(0)))
evenodd(0, s(0)) → false
evenodd(s(x), s(0)) → evenodd(x, 0)